#include "utilities.hh"
#include "cuddObj.hh"
#include <cmath>
#include <map>
#include <vector>
#include <ctime>


using namespace std;

double diffclock(clock_t clock1,clock_t clock2)
{
 double diffticks=clock1-clock2;
 double diffms=(diffticks)/(CLOCKS_PER_SEC/1000);
 
 return diffms;
}



int pow(int base, int power) {
  if (power == 0) return 1;
  if (power == 1) return base;
  if (power % 2 == 0) return pow(base * base, power / 2);
  if (power % 2 == 1) return base * pow(base * base, power / 2);
  return 0;
}



BDD *compute_reachable_states(BDD* in_st, BDD* Rt, BDDvector *v, BDDvector *pv,
                              Cudd *bddmgr,int &depth) {

  BDD * reach = new BDD();
  (*reach) = bddmgr->bddZero();

  BDD q = (*in_st);

  BDD next = bddmgr->bddZero();
  int acounter = 1;


  while ( q != (*reach) ) {
    (*reach) = q;
    BDD *tmp = new BDD(q*(*Rt));
    next = (*Exists(v, tmp,bddmgr));
    next = next.SwapVariables(*v,*pv);
    q = q + next;
    acounter++;
  }

  depth = acounter;
  return reach;

}


BDD *Exists(BDDvector *v, BDD *x, Cudd * mgr)
{
  int size = v->count();

  BDD tmp = mgr->bddOne(); // Always true

  for ( int j = 0; j < size; j++ ) {
    tmp = tmp * (*v)[j];
  }

  BDD *result = new BDD(x->ExistAbstract(tmp));
  return result;

}

BDD* check_nK(BDD *x, BDD *Ri, BDDvector *v, BDDvector *pv, Cudd * bddmgr,
              BDD *reach) {
  
  (*x) = x->SwapVariables(*v,*pv); // Now it's the next state

  BDD *tmp = new BDD((*Ri)*(*x));

  BDD *result = new BDD();
  result = Exists(pv,tmp,bddmgr); // States from which...

  return result;

}


BDD* preRt(BDD *x, BDD *Rt, BDDvector *v, BDDvector *pv, Cudd *bddmgr) {
  (*x) = x->SwapVariables(*v,*pv); // Now it's the next state
   
  BDD *tmp = new BDD((*x) * (*Rt));

  BDD *result = new BDD();

  result = Exists(pv,tmp,bddmgr);

  return result;
   
}


BDD* check_EY(BDD *x, BDD *Rt, BDDvector *v, BDDvector *pv, Cudd * bddmgr,
              BDD *reach) {
  BDD *result = new BDD(bddmgr->bddZero());

  BDD *tmp = new BDD((*Rt)*(*x));

  result = Exists(v,tmp,bddmgr); // States from which...

  (*result) = result->SwapVariables(*pv,*v);

  return result;
}

BDD* check_AY(BDD *x, BDD *Rt, BDDvector *v, BDDvector *pv, Cudd * bddmgr,
              BDD *reach) {
  // A shortcut for !EY(!..)
  BDD *result = new BDD();
  BDD tmp = !(*x);
  result = check_EY(&tmp,Rt,v,pv,bddmgr,reach);
  (*result) = (!(*result))*(*reach);
  return result;
}

vector<BDD *> * compute_EC(BDD *Ri, BDDvector *v, BDDvector *pv, Cudd * bddmgr,
                           BDD *reach) {
  vector<BDD *> *result = new vector<BDD *>();
  // Compute the set of equivalence classes for epistemic relation.
  // Equivalence states stored in a vector.

  BDD *tmp = new BDD(*Exists(pv,Ri,bddmgr));
  
  while ( (*tmp) != bddmgr->bddZero() ) {
  // Select one state
    BDD *tmp2 = new BDD();
    (*tmp2) = tmp->PickOneMinterm(*v);
    BDD *seed = new BDD((*tmp2));

  // The epistemic states equivalent to the state above
    BDD *next = new BDD((*seed)*(*Ri));
    next = Exists(v,next,bddmgr);
    (*next) = next->SwapVariables(*v,*pv);


    result->push_back(new BDD(*next));
    (*tmp) = (*tmp) - (*next);
  }
  return result;
}

BDD* K1(BDD *x, BDD *Rt, BDD *Ri, BDDvector *v, BDDvector *pv, 
        vector<BDD*> *EC, Cudd *bddmgr, BDD *reach) {
  // Compute K(1,x). Just for testing.

  // States where K(x) is true
  BDD *negx = new BDD(!(*x));
  BDD *tmp1 = new BDD(!(*check_nK(negx,Ri,v,pv,bddmgr,reach)));

  BDD *result = new BDD(bddmgr->bddZero());

  BDD *tmp = new BDD();
  BDD *tmp3 = new BDD();

  for (vector<BDD*>::iterator it = EC->begin(); it != EC->end(); it++) {
    // Building the set of states (latex mode)
    // $tmp1 \land [\bigvee\limits_{X_i \in EC} !EY(!X_i)]
    // i.e.: set of states where (1) x is known and (2) such that the
    // predecessors are members of a single equivalence class.
    
    // The set of states from where we can reach something not in (*it)
    (*tmp3) = (!(*(*it)))*(*reach);
    tmp = check_EY(tmp3,Rt,v,pv,bddmgr,reach);
    // its complement (i.e., AY(*it))
    (*tmp) = (!(*tmp))*(*reach);
    (*result)=(*result)+(*tmp);
  }
  (*result)=(*result)*(*tmp1);
  return result;  
}

BDD* K2(BDD *x, BDD *Rt, BDD *Ri, BDDvector *v, BDDvector *pv, 
        vector<BDD*> *EC, Cudd *bddmgr, BDD *reach) {
  // See K1 above. Again, just for testing.
  // Notice that K2(x) iff 
  // $K1(x) \land ( (\bigvee_i AY(AY(X_i))) \land K(x)$
  

  // States where K(x) is true
  BDD *tmp2 = new BDD(*K1(x,Rt,Ri,v,pv,EC,bddmgr,reach));

  BDD *result = new BDD(bddmgr->bddZero());

  BDD *tmp = new BDD();
 
  for (vector<BDD*>::iterator it = EC->begin(); it != EC->end(); it++) {
    tmp = check_AY((*it),Rt,v,pv,bddmgr,reach);
    tmp = check_AY(tmp,Rt,v,pv,bddmgr,reach);
    (*result)=(*result)+(*tmp);
  }
  (*result)=(*result)*(*tmp2);
  return result;  
}


BDD* Kn(int n, BDD *x, BDD *Rt, BDD *Ri, BDDvector *v, BDDvector *pv, 
        vector<BDD*> *EC, Cudd *bddmgr, BDD *reach) {
  // See K2 above. Just loop n times instead of 2. 
  // Notice that Kn(x) iff 
  // $K_{n-1}(x) \land ( (\bigvee_i AY^n(X_i)) )$
  

  // States where K(x) is true
  BDD *result = new BDD(bddmgr->bddZero());
  BDD *negx = new BDD(!(*x));
  if ( n == 0 ) {
    // Basic case, "standard" knowledge
    BDD *result = new BDD(!(*check_nK(negx,Ri,v,pv,bddmgr,reach)));
    return result;
  } else {
    // Checking depth-1
    BDD *tmp1 = new BDD(*Kn((n-1),x,Rt,Ri,v,pv,EC,bddmgr,reach));
    
    // now building the states s.t. the n predecessors are in the same
    // E.C

    BDD *tmp = new BDD();
    for (vector<BDD*>::iterator it = EC->begin(); it != EC->end(); it++) {
      tmp = check_AY((*it),Rt,v,pv,bddmgr,reach);
      // CHECK THIS!!!
      for (int i=0; i<n-1; i++) {
	tmp = check_AY(tmp,Rt,v,pv,bddmgr,reach);
      }
      (*result)=(*result)+(*tmp);
    }
    (*result)=(*result)*(*tmp1);
    return result;  
  }
}


BDD* KPR(BDD *x, BDD *Rt, BDD *Ri, BDDvector *v, BDDvector *pv, 
	 vector<BDD*> *EC, Cudd *bddmgr, BDD *reach, int depth) {
  // Knowledge for perfect recall: it's Kn for max depth 

  BDD * result = new BDD();
  (*result) = (*Kn(depth,x,Rt,Ri,v,pv,EC,bddmgr,reach));

  return result;

}



BDD* stateid_to_BDD(int stateid, BDDvector *v, Cudd *bddmgr) {
  // Convert an integer corresponding to a state id to a BDD for that
  // state. E.g., 1 -> 001, 2 ->010, 6->110 (a simple conversion)

  BDD *result = new BDD();
  *result = bddmgr->bddOne();

  for ( int i = 0; i < v->VectorSupportSize(); i++ ) {
    if ( ( stateid & ((int) pow(2.0,i)) ) != 0 ) {
      //cout << "pos" << endl;
      *result = (*result) * (*v)[i];
    }
    else {
      //cout << "neg" << endl;
      *result = (*result) * !(*v)[i];
    }
  }
  return result;
} // end stateid_to_BDD

void build_test_model(Cudd *bddmgr, BDDvector *v, BDDvector *pv, 
		      BDD *Rt, BDD *Ri, 
		      map<string, BDD*> *evaluation) {
  

  // A model with 7 states and just 1 agent:
  // S = { s0,..,s7 }
  // Rt = { (s0,s1), (s0,s2), (s0,s3), (s1,s4), (s2,s4), (s3,s5),
  //        (s4,s0), (s5,s6), (s6,s3) }
  // Equivalence classes for Ri: {s0}, {s1,s2,s3}, {s4,s6}, {s5}
  // Evaluation: a -> {s0}; b -> {s1,s2,s3}; c -> {s4,s6}; d -> {s5}

  // Just building the transition relation as above;
  (*Rt) = ((*stateid_to_BDD(0, v, bddmgr)) * (*stateid_to_BDD(1, pv, bddmgr)))
    + ((*stateid_to_BDD(0, v, bddmgr)) * (*stateid_to_BDD(2, pv, bddmgr)))
    + ((*stateid_to_BDD(0, v, bddmgr)) * (*stateid_to_BDD(3, pv, bddmgr)))
    + ((*stateid_to_BDD(1, v, bddmgr)) * (*stateid_to_BDD(4, pv, bddmgr)))
    + ((*stateid_to_BDD(2, v, bddmgr)) * (*stateid_to_BDD(4, pv, bddmgr)))
    + ((*stateid_to_BDD(3, v, bddmgr)) * (*stateid_to_BDD(5, pv, bddmgr)))
    + ((*stateid_to_BDD(4, v, bddmgr)) * (*stateid_to_BDD(0, pv, bddmgr)))
    + ((*stateid_to_BDD(5, v, bddmgr)) * (*stateid_to_BDD(6, pv, bddmgr)))
    + ((*stateid_to_BDD(6, v, bddmgr)) * (*stateid_to_BDD(3, pv, bddmgr)));

  // This is the epistemic relation for the equivalence classes above:
  (*Ri) = ((*stateid_to_BDD(0,v,bddmgr)) * (*stateid_to_BDD(0,pv,bddmgr)))
    + ((*stateid_to_BDD(1,v,bddmgr)) * (*stateid_to_BDD(1,pv,bddmgr)))    
    + ((*stateid_to_BDD(1,v,bddmgr)) * (*stateid_to_BDD(2,pv,bddmgr)))    
    + ((*stateid_to_BDD(1,v,bddmgr)) * (*stateid_to_BDD(3,pv,bddmgr)))    
    + ((*stateid_to_BDD(2,v,bddmgr)) * (*stateid_to_BDD(1,pv,bddmgr)))    
    + ((*stateid_to_BDD(2,v,bddmgr)) * (*stateid_to_BDD(2,pv,bddmgr)))    
    + ((*stateid_to_BDD(2,v,bddmgr)) * (*stateid_to_BDD(3,pv,bddmgr)))    
    + ((*stateid_to_BDD(3,v,bddmgr)) * (*stateid_to_BDD(1,pv,bddmgr)))    
    + ((*stateid_to_BDD(3,v,bddmgr)) * (*stateid_to_BDD(2,pv,bddmgr)))    
    + ((*stateid_to_BDD(3,v,bddmgr)) * (*stateid_to_BDD(3,pv,bddmgr)))    
    + ((*stateid_to_BDD(4,v,bddmgr)) * (*stateid_to_BDD(4,pv,bddmgr)))    
    + ((*stateid_to_BDD(4,v,bddmgr)) * (*stateid_to_BDD(6,pv,bddmgr)))    
    + ((*stateid_to_BDD(6,v,bddmgr)) * (*stateid_to_BDD(4,pv,bddmgr)))    
    + ((*stateid_to_BDD(6,v,bddmgr)) * (*stateid_to_BDD(6,pv,bddmgr)))    
    + ((*stateid_to_BDD(5,v,bddmgr)) * (*stateid_to_BDD(5,pv,bddmgr)));

  // And now evaluations
  (*evaluation)["a"] = stateid_to_BDD(0,v,bddmgr);
  (*evaluation)["b"] = new BDD((*stateid_to_BDD(1,v,bddmgr))
			 + (*stateid_to_BDD(2,v,bddmgr))
				 + (*stateid_to_BDD(3,v,bddmgr)));  
  (*evaluation)["c"] = new BDD((*stateid_to_BDD(4,v,bddmgr))
			 + (*stateid_to_BDD(6,v,bddmgr)));
  (*evaluation)["d"] = stateid_to_BDD(5,v,bddmgr);

} // end build_test_model



void build_deep_model(int n, Cudd *bddmgr, BDDvector *v, BDDvector *pv, 
		      BDD *Rt, BDD *Ri, 
		      map<string, BDD*> *evaluation) {

  // Build a "deep" model: a binary tree of depth n:
  //      0
  //   1     2
  //  3 4   5 6
  //    ....
  // Each layer is in the same equiv. class.  In the last layer, the
  // first half of the nodes go back to node 0; the second half goes
  // back to node 2. (thus, no KPR for the proposition defined over
  // the last layer)

  // First layer, 0->1 and 0->2
  (*Rt) = ((*stateid_to_BDD(0, v, bddmgr)) * 
	   (*stateid_to_BDD(1, pv, bddmgr))) +
    ((*stateid_to_BDD(0, v, bddmgr)) * 
     (*stateid_to_BDD(2, pv, bddmgr)));

  Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);

  //  cout << "Deep model: building the temporal relation..." << endl;
  // Temporal relation for the things in the middle
  for (int i=1; i<n; i++) {
    for (int j=pow(2,i)-1; j<pow(2,i+1)-1; j++) {
      (*Rt) += ((*stateid_to_BDD(j,v,bddmgr)) * 
		(*stateid_to_BDD((j*2)+1,pv,bddmgr))) +
	((*stateid_to_BDD(j,v,bddmgr)) * 
	 (*stateid_to_BDD((j*2)+2,pv,bddmgr)));
    }
  }

  //  cout << "... first half of last row..." << endl;
  // Temporal relation for the last row, first half:
  for (int j=pow(2,n)-1; j<(pow(2,n)+pow(2,n-1))-1; j++) {
    (*Rt) +=  ((*stateid_to_BDD(j,v,bddmgr)) * 
	       (*stateid_to_BDD(0,pv,bddmgr)));
  }

  //  cout << "... second half of last row..." << endl;
  // Temporal relation for the last row, second half:
  for (int j=(pow(2,n)+pow(2,n-1))-1; j<pow(2,n+1)-1; j++) {
    (*Rt) +=  ((*stateid_to_BDD(j,v,bddmgr)) * 
	       (*stateid_to_BDD(2,pv,bddmgr)));
  }


  //  cout << "Temporal relation done" << endl;

  //  cout << "Building the epistemic relation..." << endl;
  clock_t begin=clock();
  Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
  (*Ri) = bddmgr->bddZero();
  // Epistemic relation
  for (int i=0; i<n+1; i++) {
    Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
    for (int j=pow(2,i)-1; j<pow(2,i+1)-1; j++) {
      for (int k=pow(2,i)-1; k<pow(2,i+1)-1; k++) {
	(*Ri) +=  ((*stateid_to_BDD(j,v,bddmgr)) * 
		   (*stateid_to_BDD(k,pv,bddmgr)));
      }
    }
  }
  clock_t end=clock();
  cout << "  Epistemic construction: " <<diffclock(end,begin)<<" ms" << endl;
  // Evaluation (just the last line)
  
  (*evaluation)["a"] = stateid_to_BDD(pow(2,n)-1,v,bddmgr);
    
  for (int j=pow(2,n)-1; j<pow(2,n+1)-1; j++) {
    (*(*evaluation)["a"]) +=  (*stateid_to_BDD(j,v,bddmgr));
  }
} // End of build_deep_model


void build_wide_model(int w, int d, Cudd *bddmgr, BDDvector *v, BDDvector *pv, 
		      BDD *Rt, BDD *Ri, 
		      map<string, BDD*> *evaluation) {

  // Build a "wide" model: a tree of depth d, each node has w children:
  //    ....
  // Each layer is in the same equiv. class.  In the last layer, the
  // first half of the nodes go back to node 0; the second half goes
  // back to node 2. (thus, no KPR for the proposition defined over
  // the last layer)

  // First layer, 0->1 ... 0->w
  (*Rt) = bddmgr->bddZero();
  for (int i=1; i<=w; i++) {
    (*Rt) += ((*stateid_to_BDD(0, v, bddmgr)) * 
	      (*stateid_to_BDD(i, pv, bddmgr)));
  }

  Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
  /*
                     0                                          <-1 
     1               2             3                            <-3
 4            5        6         7        8     ....    12      <-9
13 14 15  16 17 18  19 20 21  22 23 24 25 26 27       37 38 39  <-27

   */


  //  cout << "Wide model: building the temporal relation..." << endl;
  // Temporal relation for the things in the middle
  int last = 1;
  for (int i=1; i<d; i++) {
    for (int j=last; j<=last+pow(w,i); j++) {
      for (int k=j*w+1; k<=(j+1)*w; k++) {
	(*Rt) += ((*stateid_to_BDD(j,v,bddmgr)) * 
		  (*stateid_to_BDD(k,pv,bddmgr)));
      }
    }
    last += pow(w,i);
  }

  //  cout << "... first part of last row (not exactly half)..." << endl;
  // Temporal relation for the last row, first elements:
  
  for (int j=last; j<last+pow(w,d-1); j++) {
    (*Rt) +=  ((*stateid_to_BDD(j,v,bddmgr)) * 
	       (*stateid_to_BDD(0,pv,bddmgr)));
  }

  //  cout << "... second part of last row..." << endl;
  // Temporal relation for the last row, second half:
  for (int j=last+pow(w,d-1); j<last+pow(w,d); j++) {
    (*Rt) +=  ((*stateid_to_BDD(j,v,bddmgr)) * 
	       (*stateid_to_BDD(w,pv,bddmgr)));
  }


  //  cout << "Temporal relation done" << endl;

  //  cout << "Building the epistemic relation..." << endl;
  clock_t begin=clock();

  Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
  (*Ri) = bddmgr->bddZero();
  (*Ri) += ((*stateid_to_BDD(0,v,bddmgr)) * 
	    (*stateid_to_BDD(0,pv,bddmgr)));
  // Epistemic relation
  
  last = 1;
  for (int i=1; i<=d; i++) {
    for (int j=last; j<=last+pow(w,i); j++) {
      for (int k=last; k<=last+pow(w,i); k++) {
	(*Ri) += ((*stateid_to_BDD(j,v,bddmgr)) * 
		  (*stateid_to_BDD(k,pv,bddmgr)));
      }
    }
    last += pow(w,i);
  }
  
  clock_t end=clock();
  cout << "    Epistemic construction: " <<diffclock(end,begin)<<" ms" << endl;


  // Evaluation (just the last line)

  last -= pow(w,d);

  (*evaluation)["a"] =  new BDD(bddmgr->bddZero());
    
  for (int j=last; j<=last+pow(w,d); j++) {
    (*(*evaluation)["a"]) +=  (*stateid_to_BDD(j,v,bddmgr));
  }
  //  (*evaluation)["a"]->print(2,2);
} // End of build_wide_model

